include "arithmetics/nat.ma".
include "basics/deqsets.ma". 
include "basics/lists/list.ma".
include "basics/lists/listb.ma".


(********************************************)
(********** ATOMI *************)
inductive Atom: Type[0] ≝
   Name  : nat → Atom
 | CoName: nat → Atom .

(* Atom: notation and interpretation *)
interpretation "Name" 'Name n = (Name n).
notation "hvbox(𝔸 \sub n)" with precedence 90 for @{ 'Name $n }.

(* Negative atom: notation and interpretation *)
notation "hvbox(𝔹 \sub n)" with precedence 90 for @{ 'CoName $n }.
interpretation "CoName" 'CoName n = (CoName n).

(* Per definire insiemi di nomi e co-nomi tramite funzione caratteristica
come nel seguente esempio:
definition exSetB ≝ { 𝔸 \sub 2 } ∪ {𝔹 \sub 2} .
occorre avere 'include "basics/sets.ma"' .
Non seguirò questa strada perché mi pare servano strutture in cui cercare 
effettivamente gli atomi. Ovvero servono liste su insiemi con equivalenza
decidibile, come indicato da chapter5.ma e chapter6.ma. *)

definition Atomeqb ≝ λa,b:Atom.
  match a with 
  [ Name   n ⇒ match b with [ Name   m ⇒ (eqb n m)
                              | _        ⇒ false]
  | CoName n ⇒ match b with [ CoName m ⇒ (eqb n m)
                              | _        ⇒ false]].
               
notation < "a == b" non associative 
      with precedence 45 for @{Atomeqb $a $b }.

lemma Atomeqb_true: ∀a,b. iff (Atomeqb a b = true) (a = b).
(* Ho guardato la dimostrazione del lemma 
   beqitem_true in chapter7.ma del tutorial ed ho
   provato a non saltare neanche un passo. *)
#a elim a -a
#X #b cases b -b
#Y %
[1,3,5,7: #H normalize in H; destruct 
          (* applico theorem eqb_true_to_eq: 
                        ∀n,m:nat. eqb n m = true → n = m.
             in rithmetics/nat.ma *)
          lapply (eqb_true_to_eq X Y H) -H
          #Heq <Heq @refl
|2,4,6,8: #H normalize destruct
         (* applico theorem eqb_n_n: ∀n. eqb n n = true.
            in rithmetics/nat.ma *)
          @(eqb_n_n Y)
] qed .

(* Grazie al lemma precedente ho che gli Atomi formano un insieme
con equivalenza decidibile. *)
definition AtomDeqSet ≝ mk_DeqSet Atom Atomeqb Atomeqb_true.

(* A me viene da dire che si dovrebbe poter dimostrare:
   lemma  Atomeqb_false: ∀a,b:AtomDeqSet. (eqb_false AtomDeqSet a b).
ma lo statement non piace a Matita. 
La sua 'forma esplosa' è qui sotto dimostrata semplicemente copiando 
la dimostrazione di:
   lemma eqb_false: ∀S:DeqSet.∀a,b:S. (eqb ? a b) = false ↔ a ≠ b.
in basics/deqsets.ma la quale è dimostrabile toglendo #S. *)
lemma Atomeqb_false: ∀a,b:AtomDeqSet. (eqb AtomDeqSet a b) = false ↔ a ≠ b.
#a #b % #H 
  [@(not_to_not … not_eq_true_false) #H1 <H @sym_eq @(\b H1)
  |cases (true_or_false (eqb ? a b)) // #H1 @False_ind @(absurd … (\P H1) H)
  ] qed.

(* Segue la decidibilità, anche questa copiata da basics/deqsets.ma 
ed adattata. *)
lemma Atomdec_eq: ∀a,b:AtomDeqSet. a = b ∨ a ≠ b.
#a #b cases (true_or_false (eqb ? a b)) #H
  [%1 @(\P H) | %2 @(\Pf H)] qed.

(* Prima di procedere nello sfruttare AtomDeqSet, definisco la negazione
su Atom, in modo da collegare ogni nome col suo co-nome. Immagino che poi
servirà... .*)
definition Atomneg ≝ λa:Atom.
  match a with 
  [ Name   n ⇒ CoName n
  | CoName n ⇒ Name   n  ].

lemma Atomneg_idem : ∀ a: Atom. Atomneg (Atomneg a) = a.
#a cases a #N normalize @refl qed .

(* Ho l'idea che:
   (par [𝔸_n,𝔹_m,𝔹_m,]) e (par [𝔹_m,𝔸_n,𝔹_m])   (1)
   (cop [𝔸_n,𝔹_m,𝔹_m]) e (cop [𝔹_m,𝔸_n,𝔹_m])   (2)
debbano essere in relazione di eguaglianza. Al contrario:
   (seq [𝔸_n,𝔹_m]) e (seq [𝔹_m,𝔸_n])   (3)
non lo devono essere. Ovvero vorrei sfruttare l'ordine implicito in
ogni lista per rappresentare la non commutatività del seq.

Sia (1) che (2) implicano la ncessità di poter vedere le liste di nomi e conomi
come multi-insiemi quando ad essi sia applicato uno tra par o cop. 

Segue il necessario per definire le realzioni di equivalenza corrispondenti che 
siano decidibili. In seguito proverò (forse) a descrivere l'equivalenza in maniera 
più astratta. 

Il primo passo è scrivere filter_out_firstocc una versione di 
basics/lists/list.ma/filter che elimini da una lista la sola prima occorrenza di 
un elemento x in una data lista l. *) 

(* Filters out first element occurrence. *)
let rec filter_out_fo (A:DeqSet) (x:A) (l:list A) on l : list A ≝  
 match l with
 [ nil ⇒ (nil A)
 | cons h t ⇒ if (eqb A x h) then t 
                             else (cons A h (filter_out_fo A x t)) ].

(* lemma filter_out_fo_ex0:
filter_out_fo AtomDeqSet (𝔸 \sub 1) ((𝔸 \sub 1)::[]) = []. normalize // qed . *)

(* lemma filter_out_fo_ex1:
filter_out_fo AtomDeqSet (𝔸 \sub 1) [] = []. normalize // qed . *)

lemma nil_and_nil_to_nil:  ∀A.∀l1,l2:list A.
  l1 = [] →  l2 = [] →  [] = l1@l2.
#A #l1 #l2 #l1eq #l2eq >l1eq  >l2eq normalize @refl qed.

(* filter_out_fo behaves correctly on empty lists. *)
lemma filter_out_fo_nil:
∀A:DeqSet.∀x:A.∀l:list A. filter_out_fo A x [] = [] .
#A #x #l normalize @refl qed .

(* filter_out_fo behaves correctly on a single-element list. *)
lemma filter_out_fo_single:
∀A:DeqSet.∀x:A.∀l:list A. filter_out_fo A x [x] = [] .
#A #x #l normalize
(* Sotituisce con 'true' l'equivalenza 'x==x' in un 'if x==x then ...'. 
   Sarebbe equivalente alla macro >(\b (refl ? x)). *) 
>(proj2 ?? (eqb_true ? x x) (refl ? x)) normalize @refl qed.

(* filter_out_fo erases the first occurrence
   of x in l, if x belongs to l. *)
lemma filter_out_fo_ind_exists:
∀A:DeqSet.∀x:A.∀l,r:list A.
(memb A x l=false) → (filter_out_fo A x (l@[x]@r) = (l@r)).
#A #x #l #r 
(* Induzione su l. *)
elim l 
[ (* Caso con l=[]. *)
  #xnotinl normalize
  (* Sostituzione standard di x==x con true. *) 
  >(proj2 ?? (eqb_true ? x x) (refl ? x)) normalize @refl 
| #hl #tl #ind normalize
  cases (x==hl) normalize 
  [ (* Questo sarebbe il caso (x==hl)=true che implica il voler
    dimostrare:
    (filter_out_fo A x ([x,tl]@[x]@r) = ([x,tl]@r))
    Però stiamo assumendo xnotinl cioè ((x∈l)=false).  
    Dato che (x==hl)=true è stato trasformato in true=false,
    se assumiamo tale ipotesi possiamo sfruttare destruct
    per eliminare il caso assurdo! *)
    #abs destruct
  | (* Questo sarebbe il caso (x==hl)=fasle. *) 
    normalize in ind; #H 
    >(ind H) @(eq_f2 … hl hl (tl@r) (tl@r)) @refl
  ] ] qed .

(* filter_out_fo is the identity on l, if x does not belong to l. *)
lemma filter_out_fo_ind_not_exists:
∀A:DeqSet.∀x:A.∀l:list A.
(memb A x l=false) → (filter_out_fo A x l = l).
#A #x #l
(* Induzione su l. *)
elim l 
[ (* Caso con l=[]. *)
  #xnotinl normalize @refl 
| #hl #tl #ind normalize
  cases (x==hl) normalize 
  [ (* Questo sarebbe il caso (x==hl)=true. 
    Dato che (x==hl)=true è stato trasformato in true=false,
    se assumiamo tale ipotesi possiamo sfruttare destruct
    per eliminare il caso assurdo! *)
    #abs destruct
  | (* Questo sarebbe il caso (x==hl)=fasle. *) 
    normalize in ind; #H 
    >(ind H) @(eq_f2 … hl hl (tl) (tl)) @refl
  ] ] qed .

(* Ne consegue che ListAsMultiDecSeteq, date l e l', per ogni elemento h di l,
ne cerca la prima occorrenza in l'. Trovandola la cancella. Se il risultato è
svuotare contemporaneamente l ed l', esse conicidno a meno dell'ordine 
degli elementi. *)
let rec ListAsMultiDecSeteq  (A:DeqSet) (l:list A) (l':list A) on l: bool ≝ 
  match l with
  [ nil ⇒ match l' with [ nil ⇒ true | _   ⇒ false ]
  | cons h t ⇒ match l' with 
               [ nil ⇒ false
               | _  ⇒  let r ≝ (filter_out_fo A h l') 
                       in (ListAsMultiDecSeteq  A t r) ]].

(* Alcuni esempi di funzionamento di ListAsMultiDecSeteq: 
lemma ListAsMultiDecSeteq_ex0:
ListAsMultiDecSeteq AtomDeqSet [] [] = true. normalize // qed .

lemma ListAsMultiDecSeteq_ex0':
ListAsMultiDecSeteq AtomDeqSet [] ((𝔸 \sub 1)::[]) = false. normalize // qed .

lemma ListAsMultiDecSeteq_ex0'':
ListAsMultiDecSeteq AtomDeqSet ((𝔸 \sub 1)::[]) [] = false. normalize // qed .

lemma ListAsMultiDecSeteq_ex1:
ListAsMultiDecSeteq AtomDeqSet ((𝔸 \sub 1)::[])  ((𝔸 \sub 1)::[]) = true.
normalize // qed .

lemma ListAsMultiDecSeteq_ex2:
ListAsMultiDecSeteq AtomDeqSet ((𝔸 \sub 1)::[]) ((𝔸 \sub 1)::(𝔸 \sub 2)::[]) = false.
normalize // qed .

lemma ListAsMultiDecSeteq_ex3:
ListAsMultiDecSeteq AtomDeqSet ((𝔸 \sub 1)::(𝔸 \sub 2)::[]) 
                               ((𝔸 \sub 1)::(𝔸 \sub 2)::[]) = true. normalize // qed .

lemma ListAsMultiDecSeteq_ex4:
ListAsMultiDecSeteq AtomDeqSet ((𝔸 \sub 1)::(𝔸 \sub 2)::[]) 
                               ((𝔸 \sub 2)::(𝔸 \sub 1)::[]) = true. normalize // qed .

lemma ListAsMultiDecSeteq_ex5:
ListAsMultiDecSeteq AtomDeqSet ((𝔸 \sub 2)::(𝔸 \sub 1)::(𝔸 \sub 2)::[]) 
                               ((𝔸 \sub 1)::(𝔸 \sub 2)::(𝔸 \sub 2)::[]) = true.
normalize // qed .  --------------------------------------- *)

(* Dimostrazione che ListAsMultiDecSeteq è una relazione di equivalenza. *)

lemma ListAsMultiSeteq_symm_nil_r: 
∀A:DeqSet.∀r:list A. 
(ListAsMultiDecSeteq A [ ] r = true) 
   → (ListAsMultiDecSeteq A r [ ] = true).
#A #r elim r
[// | #hr #tr  #ind normalize // ] qed.

lemma ListAsMultiSeteq_symm_l_nil: 
∀A:DeqSet.∀l:list A. 
(ListAsMultiDecSeteq A l [ ] = true) 
   → (ListAsMultiDecSeteq A [ ] l = true).
#A #l elim l [// | #hl #tl #ind normalize // ] qed.


lemma ListAsMultiDecSeteq_refl: 
∀A:DeqSet.∀l:list A. (ListAsMultiDecSeteq A l l = true).
#A #l elim l normalize
[ @refl
| #h #t #ind
  >(proj2 ?? (eqb_true ? h h) (refl ? h))
  normalize @ind ] qed .

lemma ListAsMultiSeteq_symm: 
∀A:DeqSet.∀x:A.∀m,n,p,q:list A. 
(memb A x m=false)
 → (memb A x p=false)
    → (ListAsMultiDecSeteq A (m@[x]@n) (p@[x]@q) = true) 
       → (ListAsMultiDecSeteq A (p@[x]@q) (m@[x]@n) = true).
#A #x #m #n #p #q lapply n -n lapply q -q 
elim m elim p
[1: #a #b elim a elim b normalize
    >(proj2 ?? (eqb_true ? x x) (refl ? x))
    [1,2,3: normalize
    |4:  #ha #ta normalize #Hind normalize
     #hb
     cases (true_or_false … (ha==hb)) 
     cases (true_or_false … (hb==ha)) 
     #hahbtrue #hbhatrue 
     >hahbtrue >hbhatrue normalize #c #H
     (* C'è da indovinare: *)
     check (Hind A H)
     ] 
    
|2:
|3:
|4:
] qed .




lemma ListAsMultiSeteq_symm: 
∀A:DeqSet.∀l,r:list A. 
(ListAsMultiDecSeteq A r l = true) 
   → (ListAsMultiDecSeteq A l r = true).
(* A mano farei la dimostrazione per induzione su r
procedendo per casi su r stesso. *)
#A #l #r lapply l -l elim r
[2: #hr #tr #Hind
 (* è ∀l0. 
     (ListAsMultiDecSeteq A tr l=true
             →ListAsMultiDecSeteq A l tr=true).
 Ora procedo per casi su l. *)
 #l elim l
 [2: #hl #tl #H normalize 
     cases (true_or_false … (hl==hr)) 
     cases (true_or_false … (hr==hl))
     #hrhltrue #hlhrtrue 
     >hrhltrue >hlhrtrue normalize
     [1: #H1 @(Hind tl H1)
     |2: cases (filter_out_fo A hr tl)
     |
     cases (hr::filter_out_fo A hr tl)
     cases (hl::filter_out_fo A hl tr)
     cases (hl::filter_out_fo A hr tl)
     
     |2,3,5,9: #a #b #H1 @(Hind tl H1)
     |4,6,7,10: #a #b #a' #b' #H1 @(Hind tl H1)
     |3:
     |4: ]
      
 |
 ]
|1:
]
[ (* Con r=[] la tesi è:
     (ListAsMultiDecSeteq A [] l = true) 
       → (ListAsMultiDecSeteq A l [] = true) concludo con
     ListAsMultiSeteq_symm_nil_r. *)
  @ListAsMultiSeteq_symm_nil_r
| (* Assumo r=hr::tr. *)
  #hr #tr -r
  (* La tesi diventa:
      (ListAsMultiDecSeteq A hr::tr l = true) 
        → (ListAsMultiDecSeteq A l hr::tr = true).

    A questo punto posso considerare i due casi per l. *)
  cases l -l
  [(* Se l=[] la tesi diventa:
      (ListAsMultiDecSeteq A hr::tr [] = true) 
         → (ListAsMultiDecSeteq A [] hr::tr = true)
    e concludo con ListAsMultiSeteq_symm_l_nil. *)
   #H @ListAsMultiSeteq_symm_l_nil
  | (* Assumo l=hl::tl *)
    #hl #tl 
    (* La tesi diventa:
       (ListAsMultiDecSeteq A hr::tr hl::tl = true) 
          → (ListAsMultiDecSeteq A hl::tl hr::tr = true). (2)

    Per dimostrare (2) assumo:
      #J: ListAsMultiDecSeteq A hr::tr hl::tl = true. *)
    #H #J
    (* Il goal rimane:
      (ListAsMultiDecSeteq A hl::tl hr::tr = true). (3)

    Per definizione #J equivale a:
       ListAsMultiDecSeteq tr (filter_out_fo hr hl::tl). (4) *) 
   normalize in J;
  ]
    
 [ #H @ListAsMultiSeteq_symm_nil_r
 | #hr #tr #Hind #Hind2 normalize 

 cases (true_or_false … (hr==hl))
 cases (true_or_false … (hl==hr)) normalize
 #eq1 #eq2 >eq1 >eq2 normalize
  [ /2/
  |
  |
  |
  ] 
 cases (hr==hl)
 cases (hl==hr)
 normalize
 
   cases (filter_out_fo A hr (hl::tl))
 ]

lemma ListAsMultiSeteq_symm: 
∀A:DeqSet.∀l,r:list A. 
(ListAsMultiDecSeteq A r l = true) 
   → (ListAsMultiDecSeteq A l r = true).



#A #l elim l
[ (* Caso con l=[]. *)
  normalize #r elim r 
  [ (* Caso con r=[]. *)
    normalize #taut @taut
  | (* Caso con r=hr::tr. *) 
    #hr #tr normalize #ind #taut @taut
  ]
| (* Caso con l=hl::tl. *)
  #hl #tl normalize #ind 
  #r elim r  
  [ (* Caso con r=[]. *)
    normalize #abs @abs
  | (* Caso con r=hr::tr. *) 
    #hr #tr 
    cases tr
    [ normalize cases (hr==hl)
    check sym_eq
      [ normalize
      |
      ]
        
    |
    ]
    
    
    normalize #H
    check (proj2 … (eqb_false ? hr hl) )
    
    
    
    
    #ind #taut @taut
  ]
   #H 
  
   normalize
] qed .

(* lemma ListAsMultiSeteq_tran: 
∀A:DeqSet.∀l,l',l'':list A. 

(ListAsMultiDecSeteq A l l' = true) → 
 (ListAsMultiDecSeteq A l' l'' = treu) → 
   (ListAsMultiDecSeteq A l l'' = true). *)




(* Il seguente  principio di induzione sul list DeqSet, che non mi pare essere
stato dimostrato, può essere utile. 
lemma list_ind : ∀T:DeqSet.∀l:list T.∀P:list T → Prop.
  (P []) → (∀t,h. P t → P (h::t)) → P l.
#T #l #P #Pnil #Pcons elim l [@Pnil | -Pnil #H #T @Pcons ] qed. ----------*)


(* Relazione 'astratta' ListAsMultiSeteq tra liste viste come multi insieme.
Vorrei dimostrare che ListAsMultiSeteq è una relazione di equivalenza, e che
ListaAsMultiDeqSeteq ne è una istanza decidibile. *)

inductive ListAsMultiSeteq  (A:Type[0]) : list A → list A → Prop ≝ 
  | lambaseeqbase : ListAsMultiSeteq A (nil A) (nil A)
  | lambaseeqind  : ∀l,r:list A.∀h:A.
                     ∀l1,r1,l2,r2:list A.
                      ((append A l1 (append A [h] r1)) = l) → 
                        ((append A l2 (append A [h] r2)) = r) → 
                           (ListAsMultiSeteq A (append A l1 r1)
                                               (append A l2 r2)) → 
                             (ListAsMultiSeteq A (append A l1 (append A [h] r1))
                                                 (append A l2 (append A [h] r2))).

(* lemma ListAsMultiSeteq_tran: 
∀A.∀l,l',l'':list A. ListAsMultiSeteq A l l' → 
   ListAsMultiSeteq A l' l'' → ListAsMultiSeteq A l l'' .

lemma ListAsMultiSeteq_symm:
∀A.∀l,r:list A. 
ListAsMultiSeteq A l r → ListAsMultiSeteq A r l.

lemma ListAsMultiSeteq_refl: 
∀A.∀l:list A. ListAsMultiSeteq A l l.
#A #l elim l 
[ @(lambaseeqbase A [ ] [ ]) @refl 
| #h #t #Hind 
   @(lambaseeqind A [ ] [ ] t t h) normalize @Hind ] qed.

*)

(* Il prossim passo dimostra che ListAsMultiDeqSeteq è una realizzazione 
decidibile di ListAsMultiDecSeteq.
lemma ListAtomeqb_true: 
 ∀a,b: list AtomDeqSet. 
    (ListAsMultiDecSeteq AtomDeqSet a b = true) ↔
    (ListAsMultiSeteq    AtomDeqSet  a b).  *)


(*****************************)
(******** OPERATORI **********)
inductive  Operator : Type[0] ≝
|  par : Operator
|  seq : Operator
|  cop : Operator .

definition Operatoreqb ≝ λa,b:Operator.
  match a with 
  [ par ⇒ match b with [ par ⇒ true | _ ⇒ false]
  | seq ⇒ match b with [ seq ⇒ true | _ ⇒ false]
  | cop ⇒ match b with [ cop ⇒ true | _ ⇒ false]].

lemma Operatoreqb_true: ∀a,b. 
   iff (Operatoreqb a b = true) (a = b).
#a cases a -a #b cases b -b %
[1,3,5,7,9,11,13,15,17: #H normalize in H; destruct @refl
|2,4,6,8,10,12,14,16,18: #H normalize destruct @refl
] qed .

definition OperatorDeqSet ≝ mk_DeqSet Operator Operatoreqb Operatoreqb_true.

lemma Operatoreqb_false: 
   ∀a,b:OperatorDeqSet. (eqb ? a b) = false ↔ a ≠ b.
#a #b % #H 
  [@(not_to_not … not_eq_true_false) #H1 <H @sym_eq  @(\b H1)
  |cases (true_or_false (eqb ? a b)) // #H1 @False_ind @(absurd … (\P H1) H)
  ] qed.

lemma Opeartordec_eq: ∀a,b:OperatorDeqSet. a = b ∨ a ≠ b.
#a #b cases (true_or_false (eqb ? a b)) #H
  [%1 @(\P H) | %2 @(\Pf H)] qed.

(*****************************)
(******** Strutture **********)
inductive Structure : Type[0] ≝
|  unit   : Structure
|  sbase  : Operator → list AtomDeqSet → Structure
|  sind   : Operator → list Structure  → Structure .

definition Structureqb ≝ λa,b:Structure.
  match a with 
  [ unit      ⇒ match b with 
                 [ unit ⇒ true | _    ⇒ false]
  | sbase o l ⇒ match b with 
                 [ sbase o' l' ⇒ (Operatoreqb o o') ∧ 
                                    (* Quella che segue deve essere 
                                    un po' sofisticata. *) 
                                    (ListAtomDeqSeteqb l l') 
                 | _           ⇒ false]
  | sind  o l ⇒ match b with 
                 [ sind o' l'  ⇒ (Operatoreqb o o') ∧ 
                                    (* Quella che segue deve essere 
                                     ancora più sofisticata della
                                     precedente. *) 
                                    (ListAtomDeqSeteqb l l')
                 | _           ⇒ false] ].
               
notation < "a == b" non associative with precedence 45 for @{Atomeqb $a $b }.

lemma Structureqb_true: ∀a,b. iff (Structureeqb a b = true) (a = b).
#a elim a -a
#X #b cases b -b
#Y %
[1,3,5,7: #H normalize in H; destruct 
          (* applico theorem eqb_true_to_eq: 
                        ∀n,m:nat. eqb n m = true → n = m.
             in rithmetics/nat.ma *)
          lapply (eqb_true_to_eq X Y H) -H
          #Heq <Heq @refl
|2,4,6,8: #H normalize destruct
         (* applico theorem eqb_n_n: ∀n. eqb n n = true.
            in rithmetics/nat.ma *)
          @(eqb_n_n Y)
] qed .

(* Grazie al lemma precedente ho che gli Atomi formano un insieme
con equivalenza decidibile. *)
definition AtomDeqSet ≝ mk_DeqSet Atom Atomeqb Atomeqb_true.

let rec Structureneg (s:Structure) on s : Structure ≝ 
match s with 
[ unit      ⇒ unit
| sbase o l ⇒ match o with
               [ par ⇒ (sbase cop (map ?? Atomneg l))
               | seq ⇒ (sbase seq (map ?? Atomneg l))
               | cop ⇒ (sbase par (map ?? Atomneg l))]
| sind o l  ⇒ match o with
              [ par ⇒ match l with 
                      [ nil      ⇒ sind cop []
                      | cons h t ⇒ sind cop 
                                        ((Structureneg h):: 
                                          (map ?? Structureneg t))]
              | seq ⇒ match l with 
                      [ nil      ⇒ sind seq []
                      | cons h t ⇒ sind seq 
                                        ((Structureneg h):: 
                                          (map ?? Structureneg t))]
              | cop ⇒ match l with 
                      [ nil      ⇒ sind par []
                      | cons h t ⇒ sind par 
                                        ((Structureneg h):: 
                                          (map ?? Structureneg t))]  
             ]
].


(* Il principio di induzione potrebbe essere tipo il seguente. *)
theorem Structure_induction: 
∀P:Structure → Prop. 
    P unit → 
    (∀o:Operator. P (sbase o [])) → 
    (∀o:Operator.∀l:list AtomDeqSet. P (sbase o l)) →
    (∀o:Operator. P (sind o [])) → 
    (∀o:Operator.∀h:Structure.∀t:list Structure. 
        P h → P (sind o t) → P (sind o (h::t))) → 
    (∀s:Structure. P s) .
(* da fare *)


(* check Structureneg. *)

(* Da dimostrare a pezzi sfruttando Structure_induction alla fine. *)
lemma Structureneg_idem: ∀s:Structure. Structureneg (Structureneg s) = s.
#s cases s 
[ normalize @refl ] (* Primo goal *)
#L elim L 
[1,3,5,7,9,11: normalize @eq_f @refl
|2,4,6: #Hh #Ht 
 cases Hh #N #Hind normalize
  @eq_f @eq_f  (* ??????? *)
 ]
]  qed .


definition Structureeqb ≝ λa,b:Atom.
notation < "a ≡ b" non associative with precedence 45 for @{Atomeqb $a $b }.

let rec flatten (S : DeqSet) (l : list (word S)) on l : word S ≝ 
match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].



(**********************************************************)
(* Abbozzo di una possibile strada alternativa
per definire le strutture. *)
definition Atomword ≝ list AtomDeqSet.
definition AtomBag1 ≝ [ 𝔸 \sub 1; 𝔹 \sub 2 ].

(* Unit: notation and interpretation *)
interpretation "Unit" 'Unit = (nil AtomDeqSet).
notation "𝟙" non associative with precedence 90 for @{ 'Unit }.
(* check 𝟙. *)

(* Par *)
inductive Par (A,B:Prop) : Prop ≝
    mkPar : A → B → Par A B.
(* Seq *)
inductive Seq (A,B:Prop) : Prop ≝
    mkSeq : A → B → Seq A B.
(* CoP *)
inductive CoP (A,B:Prop) : Prop ≝
    mkCoP : A → B → CoP A B.

(**********************************************************)
(* Altro abbozzo di definizione alternativa per la definizione
delle strutture. *)
definition name   ≝ λA:Type[0].λx,a:A.〈 x=a, true 〉.
interpretation "name" 'name x = (name ? x).
notation "x+" with precedence 100 for @{name $x}.  
definition coname ≝ λA:Type[0].λx,a:A.〈 x=a, false 〉.
interpretation "singleton" 'coname x = (coname ? x).
notation "x-" with precedence 100 for @{coname $x}.

(* check name.   *)
definition a_a ≝ name nat 1. definition a_b ≝ name nat 2.
definition a_c ≝ name nat 3. definition a_d ≝ name nat 4.
definition ca_a ≝ coname nat 1. definition ca_b ≝ coname nat 2.
definition ca_c ≝ coname nat 3. definition ca_d ≝ coname nat 4.

inductive operator : Type[0] ≝
  mkpar : operator
| mkcopar : operator
| mkseq : operator.  